retraction(T;f) == h:T. (x:T. (f(x) = x)  ((h(f(x))) < (h(x)))) 

latex

---

clarification:

retraction(T;f) == h:T. (x:T. (f(x) = x  T)  ((h(f(x))) < (h(x)))) 

latex

Definitions	x:A. B(x), x:AB(x), , x:A. B(x), P  Q, s = t, a < b, f(a)
FDL editor aliases	retraction